Issue3323q.agda:10,12-13
Unexpected modality/relevance annotation in (@0 b)
when checking the definition of T
